package kodkod.analysis;

import java.util.LinkedList;
import kodkod.ast.*;

public class DerivedSolutionRates {
	private static final long serialVersionUID = -6368625539935148525L;
	
	public DerivedRate plainRate;
	
	class DerivedRate {
		public DerivedRate(Node owner) { this.value = 1.0; this.owner = owner; }
		public Double value; public Node owner;
	}
	LinkedList<DerivedRate> derivedRates = new LinkedList<DerivedRate>();
	
	public DerivedSolutionRates(double value) {
		plainRate = new DerivedRate(null);
		plainRate.value = value;
	}
	
	public void newDerivedRate(Node r) {
		derivedRates.add(new DerivedRate(r));
	}
	
	public DerivedSolutionRates not() {
		plainRate.value = 1 - plainRate.value;
		for (DerivedRate rate : derivedRates) {
			rate.value = 1 - rate.value;
		}
		return this;
	}
	public DerivedSolutionRates and(DerivedSolutionRates other) {
		for (DerivedRate rate : this.derivedRates) {
			rate.value *= other.plainRate.value;
		}
		for (DerivedRate rate : other.derivedRates) {
			rate.value *= this.plainRate.value;
		}
		this.derivedRates.addAll(other.derivedRates);
		this.plainRate.value *= other.plainRate.value;
		return this;
	}
	public DerivedSolutionRates or(DerivedSolutionRates other) {
		for (DerivedRate rate : this.derivedRates) {
			rate.value = 1 - (1 - rate.value) * (1 - other.plainRate.value);
		}
		for (DerivedRate rate : other.derivedRates) {
			rate.value = 1 - (1 - rate.value) * (1 - this.plainRate.value);
		}
		this.derivedRates.addAll(other.derivedRates);
		this.plainRate.value = 1 - (1 - this.plainRate.value) * (1 - other.plainRate.value);
		return this;
	}
	public DerivedSolutionRates iff(DerivedSolutionRates other) {
		for (DerivedRate rate : this.derivedRates) {
			rate.value = rate.value * other.plainRate.value + (1 - rate.value) * (1 - other.plainRate.value);
		}
		for (DerivedRate rate : other.derivedRates) {
			rate.value = rate.value * this.plainRate.value + (1 - rate.value) * (1 - this.plainRate.value);
		}
		this.derivedRates.addAll(other.derivedRates);
		this.plainRate.value = this.plainRate.value * other.plainRate.value + (1 - this.plainRate.value) * (1 - other.plainRate.value);
		return this;
	}
	public DerivedSolutionRates implies(DerivedSolutionRates other) {
		for (DerivedRate rate : this.derivedRates) {
			rate.value = 1 - rate.value * (1 - other.plainRate.value);
		}
		for (DerivedRate rate : other.derivedRates) {
			rate.value = 1 - (1 - rate.value) * this.plainRate.value;
		}
		this.derivedRates.addAll(other.derivedRates);
		this.plainRate.value = 1 - this.plainRate.value * (1 - other.plainRate.value);
		return this;
	}
	public DerivedSolutionRates pow(int p) {
		plainRate.value = Math.pow(plainRate.value, p);
		for (DerivedRate rate : derivedRates) {
			rate.value = Math.pow(rate.value, p);
		}
		return this;
	}
}